REF, NoConds
\\[0ex]HypSubst' \$dir \$a \$b
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$((if (first\_bool \$dir:b) then HypSubst' else RevHypSubst') ( \$a)( \$b))$\cdot$